[ refactor ] Data.Fin.Properties of decidable equality, plus knock-ons
#2740
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This was referenced Jun 21, 2025
|
In the absence of a review yet, I'll lift out the bug fixes as a separate PR, as per @JacquesCarette 's comment on #2743 |
JacquesCarette
requested changes
Jun 26, 2025
MatthewDaggitt
requested changes
Jul 2, 2025
| punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ | ||
| π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ | ||
| π ⟨$⟩ʳ j ∎ | ||
| punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ |
There was a problem hiding this comment.
This is funny alignment.
| ≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ | ||
|
|
||
| ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq | ||
| ≟-diag = ≡-≟-identity _≟_ |
There was a problem hiding this comment.
I would vote for calling this ≟-diag-≡ and ≟-off-diag as ≟-diag-≢ for consistency? Actually do we even need the diag in the names? Doesn't really do much...
| @@ -42,17 +34,31 @@ transpose i j k with does (k ≟ i) | |||
| -- Properties | |||
| ------------------------------------------------------------------------ | |||
|
|
|||
| transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j | |||
There was a problem hiding this comment.
Normal naming conventions would probably be transpose[i,i,j]≡j? Same for the three below?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR supersedes the knock-on changes for
Permutationin #2738 and adds some new lemmas abouttransposewhich simplify the dependency graph. The contribution can be seen as a belated corollary to the changes introduced in #645 / #1732 .Downstream, we might want to revisit the dependency graph now between
Relation.Nullary.DecidableAxiom.UniquenessOfIdentityProofsRelation.Binary.PropositionalEqualityin putting these pieces together?
Outstanding (naming) issue: I followed the existing
Data.Nat.Properties.≟-diagconvention inData.Fin.Properties, and then backported thereflinstantiation of this toData.Nat.Properties.≟-diag-refl... but it occurs to me that it's hard to imagine instances of≟-diagwhich would use a general equality, and even if they were to, the use ofdiagought (?) to be a codeword for a repeated argument/reflexive equality? I just couldn't face the deprecation headache though... so a v3.0 downstreambreakingchange might be in order?